($\lambda$$A$,${\it as}$,$n$,$z$. firstn($n$;${\it as}$)) $\in$ $A$:Type$\rightarrow$($A$ List)$\rightarrow\mathbb{Z}\rightarrow\downarrow$True$\rightarrow$($A$ List)